<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Table of contents</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>

<script>

$(document).ready(function() {

    $("#accordion").show().accordion({
        autoHeight: false
    });

    $("#accordion div").css({ 'height': 'auto' });
});      


$( function() {
    var icons = {
      header: "ui-icon-circle-arrow-e",
      activeHeader: "ui-icon-circle-arrow-s"
    };
    
    $( "#accordion" ).accordion({
      icons: icons
    });
    $("#accordion").accordion({collapsible : true, active : 'none'});

    $( "#toggle" ).button().on( "click", function() {
      if ( $( "#accordion" ).accordion( "option", "icons" ) ) {
        $( "#accordion" ).accordion( "option", "icons", null );
      } else {
        $( "#accordion" ).accordion( "option", "icons", icons );
      }
    });
  } );
  </script>
<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: Logical Foundations</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>Table of Contents</li></a>
   <a href='coqindex.html'><li class='section_name'>Index</li></a>
   <a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</div>
</a></div>

<div id="main">

<div id="toc">
<div id="accordion">
<h2><a href="Preface.html">Preface</a></h2>
<div>
<ul class="doclist">
<li><a href="Preface.html">Top</a>
<li><a href="Preface.html#lab1">Welcome</a>

</li>
<li><a href="Preface.html#lab2">Overview</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab3">Logic</a>

</li>
<li><a href="Preface.html#lab4">Proof Assistants</a>

</li>
<li><a href="Preface.html#lab5">Functional Programming</a>

</li>
<li><a href="Preface.html#lab6">Further Reading</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab7">Practicalities</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab8">Chapter Dependencies</a>

</li>
<li><a href="Preface.html#lab9">System Requirements</a>

</li>
<li><a href="Preface.html#lab10">Exercises</a>

</li>
<li><a href="Preface.html#lab11">Downloading the Coq Files</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab12">Resources</a>
<div>
<ul class="doclist">
<li><a href="Preface.html#lab13">Sample Exams</a>

</li>
<li><a href="Preface.html#lab14">Lecture Videos</a>

</li>
</ul>
</div>

</li>
<li><a href="Preface.html#lab15">Note for Instructors</a>

</li>
<li><a href="Preface.html#lab16">Translations</a>

</li>
<li><a href="Preface.html#lab17">Thanks</a>

</li>
</ul>
</div>
<h2><a href="Basics.html">Functional Programming in Coq&nbsp;&nbsp;&nbsp;&nbsp;(<i>Basics</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Basics.html">Top</a>
<li><a href="Basics.html#lab18">Introduction</a>

</li>
<li><a href="Basics.html#lab19">Data and Functions</a>
<div>
<ul class="doclist">
<li><a href="Basics.html#lab20">Enumerated Types</a>

</li>
<li><a href="Basics.html#lab21">Days of the Week</a>

</li>
<li><a href="Basics.html#lab22">Homework Submission Guidelines</a>

</li>
<li><a href="Basics.html#lab23">Booleans</a>

</li>
<li><a href="Basics.html#lab26">Types</a>

</li>
<li><a href="Basics.html#lab27">New Types from Old</a>

</li>
<li><a href="Basics.html#lab28">Tuples</a>

</li>
<li><a href="Basics.html#lab29">Modules</a>

</li>
<li><a href="Basics.html#lab30">Numbers</a>

</li>
</ul>
</div>

</li>
<li><a href="Basics.html#lab33">Proof by Simplification</a>

</li>
<li><a href="Basics.html#lab34">Proof by Rewriting</a>

</li>
<li><a href="Basics.html#lab37">Proof by Case Analysis</a>
<div>
<ul class="doclist">
<li><a href="Basics.html#lab40">More on Notation (Optional)</a>

</li>
<li><a href="Basics.html#lab41">Fixpoints and Structural Recursion (Optional)</a>

</li>
</ul>
</div>

</li>
<li><a href="Basics.html#lab43">More Exercises</a>

</li>
</ul>
</div>
<h2><a href="Induction.html">Proof by Induction&nbsp;&nbsp;&nbsp;&nbsp;(<i>Induction</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Induction.html">Top</a>
<li><a href="Induction.html#lab48">Proof by Induction</a>

</li>
<li><a href="Induction.html#lab53">Proofs Within Proofs</a>

</li>
<li><a href="Induction.html#lab54">Formal vs. Informal Proof</a>

</li>
<li><a href="Induction.html#lab57">More Exercises</a>

</li>
</ul>
</div>
<h2><a href="Lists.html">Working with Structured Data&nbsp;&nbsp;&nbsp;&nbsp;(<i>Lists</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Lists.html">Top</a>
<li><a href="Lists.html#lab64">Pairs of Numbers</a>

</li>
<li><a href="Lists.html#lab67">Lists of Numbers</a>

</li>
<li><a href="Lists.html#lab79">Reasoning About Lists</a>
<div>
<ul class="doclist">
<li><a href="Lists.html#lab81">Induction on Lists</a>

</li>
<li><a href="Lists.html#lab84"><span class="inlinecode"><span class="id" type="var">Search</span></span></a>

</li>
<li><a href="Lists.html#lab85">List Exercises, Part 1</a>

</li>
<li><a href="Lists.html#lab88">List Exercises, Part 2</a>

</li>
</ul>
</div>

</li>
<li><a href="Lists.html#lab93">Options</a>

</li>
<li><a href="Lists.html#lab96">Partial Maps</a>

</li>
</ul>
</div>
<h2><a href="Poly.html">Polymorphism and Higher-Order Functions&nbsp;&nbsp;&nbsp;&nbsp;(<i>Poly</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Poly.html">Top</a>
<li><a href="Poly.html#lab101">Polymorphism</a>
<div>
<ul class="doclist">
<li><a href="Poly.html#lab102">Polymorphic Lists</a>

</li>
<li><a href="Poly.html#lab111">Polymorphic Pairs</a>

</li>
<li><a href="Poly.html#lab114">Polymorphic Options</a>

</li>
</ul>
</div>

</li>
<li><a href="Poly.html#lab116">Functions as Data</a>
<div>
<ul class="doclist">
<li><a href="Poly.html#lab117">Higher-Order Functions</a>

</li>
<li><a href="Poly.html#lab118">Filter</a>

</li>
<li><a href="Poly.html#lab119">Anonymous Functions</a>

</li>
<li><a href="Poly.html#lab122">Map</a>

</li>
<li><a href="Poly.html#lab127">Fold</a>

</li>
<li><a href="Poly.html#lab129">Functions That Construct Functions</a>

</li>
</ul>
</div>

</li>
<li><a href="Poly.html#lab130">Additional Exercises</a>

</li>
</ul>
</div>
<h2><a href="Tactics.html">More Basic Tactics&nbsp;&nbsp;&nbsp;&nbsp;(<i>Tactics</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Tactics.html">Top</a>
<li><a href="Tactics.html#lab139">The <span class="inlinecode"><span class="id" type="tactic">apply</span></span> Tactic</a>

</li>
<li><a href="Tactics.html#lab143">The <span class="inlinecode"><span class="id" type="tactic">apply</span></span> <span class="inlinecode"><span class="id" type="keyword">with</span></span> Tactic</a>

</li>
<li><a href="Tactics.html#lab145">The <span class="inlinecode"><span class="id" type="tactic">injection</span></span> and <span class="inlinecode"><span class="id" type="tactic">discriminate</span></span> Tactics</a>

</li>
<li><a href="Tactics.html#lab148">Using Tactics on Hypotheses</a>

</li>
<li><a href="Tactics.html#lab150">Varying the Induction Hypothesis</a>

</li>
<li><a href="Tactics.html#lab154">Unfolding Definitions</a>

</li>
<li><a href="Tactics.html#lab155">Using <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> on Compound Expressions</a>

</li>
<li><a href="Tactics.html#lab158">Review</a>

</li>
<li><a href="Tactics.html#lab159">Additional Exercises</a>

</li>
</ul>
</div>
<h2><a href="Logic.html">Logic in Coq&nbsp;&nbsp;&nbsp;&nbsp;(<i>Logic</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Logic.html">Top</a>
<li><a href="Logic.html#lab166">Logical Connectives</a>
<div>
<ul class="doclist">
<li><a href="Logic.html#lab167">Conjunction</a>

</li>
<li><a href="Logic.html#lab171">Disjunction</a>

</li>
<li><a href="Logic.html#lab174">Falsehood and Negation</a>

</li>
<li><a href="Logic.html#lab180">Truth</a>

</li>
<li><a href="Logic.html#lab181">Logical Equivalence</a>

</li>
<li><a href="Logic.html#lab184">Existential Quantification</a>

</li>
</ul>
</div>

</li>
<li><a href="Logic.html#lab187">Programming with Propositions</a>

</li>
<li><a href="Logic.html#lab192">Applying Theorems to Arguments</a>

</li>
<li><a href="Logic.html#lab193">Coq vs. Set Theory</a>
<div>
<ul class="doclist">
<li><a href="Logic.html#lab194">Functional Extensionality</a>

</li>
<li><a href="Logic.html#lab196">Propositions and Booleans</a>

</li>
<li><a href="Logic.html#lab202">Classical vs. Constructive Logic</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="IndProp.html">Inductively Defined Propositions&nbsp;&nbsp;&nbsp;&nbsp;(<i>IndProp</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="IndProp.html">Top</a>
<li><a href="IndProp.html#lab206">Inductively Defined Propositions</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab207">Inductive Definition of Evenness</a>

</li>
</ul>
</div>

</li>
<li><a href="IndProp.html#lab209">Using Evidence in Proofs</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab210">Inversion on Evidence</a>

</li>
<li><a href="IndProp.html#lab213">Induction on Evidence</a>

</li>
</ul>
</div>

</li>
<li><a href="IndProp.html#lab218">Inductive Relations</a>

</li>
<li><a href="IndProp.html#lab227">Case Study: Regular Expressions</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab231">The <span class="inlinecode"><span class="id" type="var">remember</span></span> Tactic</a>

</li>
</ul>
</div>

</li>
<li><a href="IndProp.html#lab234">Case Study: Improving Reflection</a>

</li>
<li><a href="IndProp.html#lab237">Additional Exercises</a>
<div>
<ul class="doclist">
<li><a href="IndProp.html#lab245">Extended Exercise: A Verified Regular-Expression Matcher</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Maps.html">Total and Partial Maps&nbsp;&nbsp;&nbsp;&nbsp;(<i>Maps</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Maps.html">Top</a>
<li><a href="Maps.html#lab254">The Coq Standard Library</a>

</li>
<li><a href="Maps.html#lab255">Identifiers</a>

</li>
<li><a href="Maps.html#lab256">Total Maps</a>

</li>
<li><a href="Maps.html#lab264">Partial maps</a>

</li>
</ul>
</div>
<h2><a href="ProofObjects.html">The Curry-Howard Correspondence&nbsp;&nbsp;&nbsp;&nbsp;(<i>ProofObjects</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="ProofObjects.html">Top</a>
<li><a href="ProofObjects.html#lab265">Proof Scripts</a>

</li>
<li><a href="ProofObjects.html#lab267">Quantifiers, Implications, Functions</a>

</li>
<li><a href="ProofObjects.html#lab268">Programming with Tactics</a>

</li>
<li><a href="ProofObjects.html#lab269">Logical Connectives as Inductive Types</a>
<div>
<ul class="doclist">
<li><a href="ProofObjects.html#lab270">Conjunction</a>

</li>
<li><a href="ProofObjects.html#lab272">Disjunction</a>

</li>
<li><a href="ProofObjects.html#lab274">Existential Quantification</a>

</li>
<li><a href="ProofObjects.html#lab276"><span class="inlinecode"><span class="id" type="var">True</span></span> and <span class="inlinecode"><span class="id" type="var">False</span></span></a>

</li>
</ul>
</div>

</li>
<li><a href="ProofObjects.html#lab277">Equality</a>
<div>
<ul class="doclist">
<li><a href="ProofObjects.html#lab280">Inversion, Again</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="IndPrinciples.html">Induction Principles&nbsp;&nbsp;&nbsp;&nbsp;(<i>IndPrinciples</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="IndPrinciples.html">Top</a>
<li><a href="IndPrinciples.html#lab281">Basics</a>

</li>
<li><a href="IndPrinciples.html#lab287">Polymorphism</a>

</li>
<li><a href="IndPrinciples.html#lab292">Induction Hypotheses</a>

</li>
<li><a href="IndPrinciples.html#lab293">More on the <span class="inlinecode"><span class="id" type="tactic">induction</span></span> Tactic</a>

</li>
<li><a href="IndPrinciples.html#lab295">Induction Principles in <span class="inlinecode"><span class="id" type="keyword">Prop</span></span></a>

</li>
<li><a href="IndPrinciples.html#lab296">Formal vs. Informal Proofs by Induction</a>
<div>
<ul class="doclist">
<li><a href="IndPrinciples.html#lab297">Induction Over an Inductively Defined Set</a>

</li>
<li><a href="IndPrinciples.html#lab298">Induction Over an Inductively Defined Proposition</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Rel.html">Properties of Relations&nbsp;&nbsp;&nbsp;&nbsp;(<i>Rel</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Rel.html">Top</a>
<li><a href="Rel.html#lab299">Relations</a>

</li>
<li><a href="Rel.html#lab300">Basic Properties</a>

</li>
<li><a href="Rel.html#lab317">Reflexive, Transitive Closure</a>

</li>
</ul>
</div>
<h2><a href="Imp.html">Simple Imperative Programs&nbsp;&nbsp;&nbsp;&nbsp;(<i>Imp</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Imp.html">Top</a>
<li><a href="Imp.html#lab320">Arithmetic and Boolean Expressions</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab321">Syntax</a>

</li>
<li><a href="Imp.html#lab322">Evaluation</a>

</li>
<li><a href="Imp.html#lab323">Optimization</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab324">Coq Automation</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab325">Tacticals</a>

</li>
<li><a href="Imp.html#lab332">Defining New Tactic Notations</a>

</li>
<li><a href="Imp.html#lab333">The <span class="inlinecode"><span class="id" type="tactic">omega</span></span> Tactic</a>

</li>
<li><a href="Imp.html#lab334">A Few More Handy Tactics</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab335">Evaluation as a Relation</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab336">Inference Rule Notation</a>

</li>
<li><a href="Imp.html#lab338">Equivalence of the Definitions</a>

</li>
<li><a href="Imp.html#lab340">Computational vs. Relational Definitions</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab341">Expressions With Variables</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab342">States</a>

</li>
<li><a href="Imp.html#lab343">Syntax</a>

</li>
<li><a href="Imp.html#lab344">Notations</a>

</li>
<li><a href="Imp.html#lab345">Evaluation</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab346">Commands</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab347">Syntax</a>

</li>
<li><a href="Imp.html#lab348">Desugaring notations</a>

</li>
<li><a href="Imp.html#lab349">The <span class="inlinecode"><span class="id" type="var">Locate</span></span> command</a>

</li>
<li><a href="Imp.html#lab352">More Examples</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab355">Evaluating Commands</a>
<div>
<ul class="doclist">
<li><a href="Imp.html#lab356">Evaluation as a Function (Failed Attempt)</a>

</li>
<li><a href="Imp.html#lab357">Evaluation as a Relation</a>

</li>
<li><a href="Imp.html#lab361">Determinism of Evaluation</a>

</li>
</ul>
</div>

</li>
<li><a href="Imp.html#lab362">Reasoning About Imp Programs</a>

</li>
<li><a href="Imp.html#lab367">Additional Exercises</a>

</li>
</ul>
</div>
<h2><a href="ImpParser.html">Lexing and Parsing in Coq&nbsp;&nbsp;&nbsp;&nbsp;(<i>ImpParser</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="ImpParser.html">Top</a>
<li><a href="ImpParser.html#lab375">Internals</a>
<div>
<ul class="doclist">
<li><a href="ImpParser.html#lab376">Lexical Analysis</a>

</li>
<li><a href="ImpParser.html#lab377">Parsing</a>

</li>
</ul>
</div>

</li>
<li><a href="ImpParser.html#lab381">Examples</a>

</li>
</ul>
</div>
<h2><a href="ImpCEvalFun.html">An Evaluation Function for Imp&nbsp;&nbsp;&nbsp;&nbsp;(<i>ImpCEvalFun</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="ImpCEvalFun.html">Top</a>
<li><a href="ImpCEvalFun.html#lab382">A Broken Evaluator</a>

</li>
<li><a href="ImpCEvalFun.html#lab383">A Step-Indexed Evaluator</a>

</li>
<li><a href="ImpCEvalFun.html#lab386">Relational vs. Step-Indexed Evaluation</a>

</li>
<li><a href="ImpCEvalFun.html#lab389">Determinism of Evaluation Again</a>

</li>
</ul>
</div>
<h2><a href="Extraction.html">Extracting ML from Coq&nbsp;&nbsp;&nbsp;&nbsp;(<i>Extraction</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Extraction.html">Top</a>
<li><a href="Extraction.html#lab390">Basic Extraction</a>

</li>
<li><a href="Extraction.html#lab391">Controlling Extraction of Specific Types</a>

</li>
<li><a href="Extraction.html#lab392">A Complete Example</a>

</li>
<li><a href="Extraction.html#lab393">Discussion</a>

</li>
<li><a href="Extraction.html#lab394">Going Further</a>

</li>
</ul>
</div>
<h2><a href="Auto.html">More Automation&nbsp;&nbsp;&nbsp;&nbsp;(<i>Auto</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Auto.html">Top</a>
<li><a href="Auto.html#lab395">The <span class="inlinecode"><span class="id" type="tactic">auto</span></span> Tactic</a>

</li>
<li><a href="Auto.html#lab396">Searching For Hypotheses</a>
<div>
<ul class="doclist">
<li><a href="Auto.html#lab397">The <span class="inlinecode"><span class="id" type="tactic">eapply</span></span> and <span class="inlinecode"><span class="id" type="tactic">eauto</span></span> variants</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="Postscript.html">Postscript</a></h2>
<div>
<ul class="doclist">
<li><a href="Postscript.html">Top</a>
<li><a href="Postscript.html#lab398">Looking Back</a>

</li>
<li><a href="Postscript.html#lab399">Looking Forward</a>

</li>
<li><a href="Postscript.html#lab400">Other sources</a>

</li>
</ul>
</div>
<h2><a href="Bib.html">Bibliography&nbsp;&nbsp;&nbsp;&nbsp;(<i>Bib</i>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Bib.html">Top</a>
<li><a href="Bib.html#lab401">Resources cited in this volume</a>

</li>
</ul>
</div>
</div>
</div>

</div>

</div>
</body>
</html>